(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(x, y) → g1(x, x, y)
f(x, y) → g1(y, x, x)
f(x, y) → g2(x, y, y)
f(x, y) → g2(y, y, x)
g1(x, x, y) → h(x, y)
g1(y, x, x) → h(x, y)
g2(x, y, y) → h(x, y)
g2(y, y, x) → h(x, y)
h(x, x) → x

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1) → g1(z0, z0, z1)
f(z0, z1) → g1(z1, z0, z0)
f(z0, z1) → g2(z0, z1, z1)
f(z0, z1) → g2(z1, z1, z0)
g1(z0, z0, z1) → h(z0, z1)
g1(z0, z1, z1) → h(z1, z0)
g2(z0, z1, z1) → h(z0, z1)
g2(z0, z0, z1) → h(z1, z0)
h(z0, z0) → z0
Tuples:

F(z0, z1) → c(G1(z0, z0, z1))
F(z0, z1) → c1(G1(z1, z0, z0))
F(z0, z1) → c2(G2(z0, z1, z1))
F(z0, z1) → c3(G2(z1, z1, z0))
G1(z0, z0, z1) → c4(H(z0, z1))
G1(z0, z1, z1) → c5(H(z1, z0))
G2(z0, z1, z1) → c6(H(z0, z1))
G2(z0, z0, z1) → c7(H(z1, z0))
S tuples:

F(z0, z1) → c(G1(z0, z0, z1))
F(z0, z1) → c1(G1(z1, z0, z0))
F(z0, z1) → c2(G2(z0, z1, z1))
F(z0, z1) → c3(G2(z1, z1, z0))
G1(z0, z0, z1) → c4(H(z0, z1))
G1(z0, z1, z1) → c5(H(z1, z0))
G2(z0, z1, z1) → c6(H(z0, z1))
G2(z0, z0, z1) → c7(H(z1, z0))
K tuples:none
Defined Rule Symbols:

f, g1, g2, h

Defined Pair Symbols:

F, G1, G2

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 8 trailing nodes:

F(z0, z1) → c(G1(z0, z0, z1))
G1(z0, z1, z1) → c5(H(z1, z0))
G2(z0, z1, z1) → c6(H(z0, z1))
F(z0, z1) → c3(G2(z1, z1, z0))
F(z0, z1) → c2(G2(z0, z1, z1))
F(z0, z1) → c1(G1(z1, z0, z0))
G1(z0, z0, z1) → c4(H(z0, z1))
G2(z0, z0, z1) → c7(H(z1, z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1) → g1(z0, z0, z1)
f(z0, z1) → g1(z1, z0, z0)
f(z0, z1) → g2(z0, z1, z1)
f(z0, z1) → g2(z1, z1, z0)
g1(z0, z0, z1) → h(z0, z1)
g1(z0, z1, z1) → h(z1, z0)
g2(z0, z1, z1) → h(z0, z1)
g2(z0, z0, z1) → h(z1, z0)
h(z0, z0) → z0
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

f, g1, g2, h

Defined Pair Symbols:none

Compound Symbols:none

(5) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(6) BOUNDS(O(1), O(1))